Inference at * 1 
Iof proof for Lemma gen hyp tp:



1. A : Type
2. e : A
3. H : AType
4. z : H(e)
  z  0 

latex

 by PushArgs 
[`x`,term_to_arg x 
;`e`,term_to_arg e 
;`A`,term_to_arg A 
;`UH`,term_to_arg 
;Type 
;`UA`,term_to_arg Type 
;`i`,int_to_arg 4] 

latex

;1: 

;1:   z  0
;.

Definitions

Type